$\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)). p{-}inject($A$;$A$;$f$) $\Rightarrow$ ($\forall$$n$:$\mathbb{N}$. p{-}inject($A$;$A$;$f$\^{}$n$))